/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

#pragma once

#include <autoconf.h>

#define TLS_GDT_ENTRY   7
#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3)

#define IPCBUF_GDT_ENTRY    8
#define IPCBUF_GDT_SELECTOR ((IPCBUF_GDT_ENTRY << 3) | 3)

#define seL4_DataFault 0
#define seL4_InstructionFault 1

/* for x86-64, the large page size is 2 MiB and huge page size is 1 GiB */
#define seL4_WordBits           64  /*Z 机器字位数 */
#define seL4_WordSizeBits       3   /*Z 机器字字节数=2^3 */
#define seL4_PageBits           12  /*Z 页大小4K */
#define seL4_SlotBits           5   /*Z 每个CSlot大小为32字节 */
#if CONFIG_XSAVE_SIZE >= 832
#define seL4_TCBBits            12
#else
#define seL4_TCBBits            11  /*Z 每个线程控制块(TCB)2K */
#endif
#define seL4_EndpointBits       4   /*Z 端点对象的大小，2个u64 */
#ifdef CONFIG_KERNEL_MCS
#define seL4_NotificationBits   6
#define seL4_ReplyBits          5
#else
#define seL4_NotificationBits   5   /*Z 通知对象的大小，4个u64 */
#endif
/*Z 第四级页表：Page table */
#define seL4_PageTableBits      12      /*Z 四级页表4K大小 */
#define seL4_PageTableEntryBits 3       /*Z 四级页表项8字节 */
#define seL4_PageTableIndexBits 9       /*Z 四级页表512项 */
/*Z 第三级页表：Page directory */
#define seL4_PageDirBits        12      /*Z 三级页表4K大小 */
#define seL4_PageDirEntryBits   3       /*Z 三级页表项8字节 */
#define seL4_PageDirIndexBits   9       /*Z 三级页表512项 */
/*Z 第二级页表：Page-directory-pointer table */
#define seL4_PDPTBits           12      /*Z 二级页表4K大小 */
#define seL4_PDPTEntryBits      3       /*Z 二级页表项8字节 */
#define seL4_PDPTIndexBits      9       /*Z 二级页表512项 */
/*Z 第一级页表：PML4 table */
#define seL4_PML4Bits           12      /*Z 一级页表4K大小 */
#define seL4_PML4EntryBits      3       /*Z 一级页表项8字节 */
#define seL4_PML4IndexBits      9       /*Z 一级页表512项 */
#define seL4_VSpaceBits seL4_PML4Bits   /*Z 12。VSpace就是一级页表 */

#define seL4_IOPageTableBits    12      /*Z IOMMU页表大小 */
#define seL4_LargePageBits      21      /*Z 64位系统的大页2M */
#define seL4_HugePageBits       30      /*Z 巨页大小1G */
#define seL4_NumASIDPoolsBits    3      /*Z ASID(PCID) pool选择位(最多8个池) */
#define seL4_ASIDPoolBits       12      /*Z ASID(PCID) pool位数(最多4096个ID) */
#define seL4_ASIDPoolIndexBits 9        /*Z ASID(PCID) pool内索引位(每池最多512项，占4K) */

/* Untyped size limits */
#define seL4_MinUntypedBits 4           /*Z 未映射内存最小16字节 */
#define seL4_MaxUntypedBits 47          /*Z 未映射内存最大2^47字节 */

#ifndef __ASSEMBLER__

SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits);
SEL4_SIZE_SANITY(seL4_PDPTEntryBits, seL4_PDPTIndexBits, seL4_PDPTBits);
SEL4_SIZE_SANITY(seL4_PML4EntryBits, seL4_PML4IndexBits, seL4_PML4Bits);
SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
/*Z 页错误类IPC消息的寄存器(IPC buffer)索引 */
enum {
    seL4_VMFault_IP,            /*Z 发生错误时的指令地址 */
    seL4_VMFault_Addr,          /*Z 发生错误时的虚拟地址 */
    seL4_VMFault_PrefetchFault, /*Z 指示是否指令预取错误 */
    seL4_VMFault_FSR,           /*Z 硬件产生的错误码 */
    seL4_VMFault_Length,
    SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
} seL4_VMFault_Msg;
/*Z 用于未知系统调用类错误IPC消息的寄存器索引转换 */
enum {
    seL4_UnknownSyscall_RAX,
    seL4_UnknownSyscall_RBX,
    seL4_UnknownSyscall_RCX,
    seL4_UnknownSyscall_RDX,
    seL4_UnknownSyscall_RSI,
    seL4_UnknownSyscall_RDI,
    seL4_UnknownSyscall_RBP,
    seL4_UnknownSyscall_R8,
    seL4_UnknownSyscall_R9,
    seL4_UnknownSyscall_R10,
    seL4_UnknownSyscall_R11,
    seL4_UnknownSyscall_R12,
    seL4_UnknownSyscall_R13,
    seL4_UnknownSyscall_R14,
    seL4_UnknownSyscall_R15,
    seL4_UnknownSyscall_FaultIP,
    seL4_UnknownSyscall_SP,
    seL4_UnknownSyscall_FLAGS,
    seL4_UnknownSyscall_Syscall,
    seL4_UnknownSyscall_Length,
    SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg)
} seL4_UnknownSyscall_Msg;

enum {
    seL4_UserException_FaultIP,
    seL4_UserException_SP,
    seL4_UserException_FLAGS,
    seL4_UserException_Number,
    seL4_UserException_Code,
    seL4_UserException_Length,
    SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg)
} seL4_UserException_Msg;

#ifdef CONFIG_KERNEL_MCS
enum {
    seL4_Timeout_Data,
    seL4_Timeout_Consumed,
    seL4_Timeout_Length,
    SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg)
} seL4_TimeoutMsg;

enum {
    seL4_TimeoutReply_FaultIP,
    seL4_TimeoutReply_RSP,
    seL4_TimeoutReply_FLAGS,
    seL4_TimeoutReply_RAX,
    seL4_TimeoutReply_RBX,
    seL4_TimeoutReply_RCX,
    seL4_TimeoutReply_RDX,
    seL4_TimeoutReply_RSI,
    seL4_TimeoutReply_RDI,
    seL4_TimeoutReply_RBP,
    seL4_TimeoutReply_R8,
    seL4_TimeoutReply_R9,
    seL4_TimeoutReply_R10,
    seL4_TimeoutReply_R11,
    seL4_TimeoutReply_R12,
    seL4_TimeoutReply_R13,
    seL4_TimeoutReply_R14,
    seL4_TimeoutReply_R15,
    seL4_TimeoutReply_TLS_BASE,
    seL4_TimeoutReply_Length,
    SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg)
} seL4_TimeoutReply_Msg;
#endif
#endif /* __ASSEMBLER__ */
#define seL4_FastMessageRegisters 4 /*Z TCB上下文中用于消息的寄存器数量 */
/*Z 应该是用户空间IPC buffer大小 */
/* IPC buffer is 1024 bytes, giving size bits of 10 */
#define seL4_IPCBufferSizeBits 10

/* First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0x00007ffffffff000

